T:Type, eq, r:(TT).
(a, b:T. ((eq(a,b)))  (a = b))
 Linorder(T;a,b.(r(a,b)))
 (x:T, L:(T List).
 sorted-by(x,y. (r(x,y));L)  sorted-by(x,y. (r(x,y));insert-by(eq;r;x;L))) 

latex

Definitions

type List, t  T, s = t, Type, x:AB(x), x:A. B(x), Linorder(T;x,y.R(x;y)), b, sorted-by(R;L), insert-by(eq;r;x;l), P  Q, f(a), , x.A(x), x,y. t(x;y), P  Q, , ||as||, a < b, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , {i..j}, Void, , [], x:A  B(x), l[i], #$n, [car / cdr], P  Q, rec-case(a) of [] => s | x::y => z.t(x;y;z), xL. P(x), |g|, S  T, Unit, left + right, case b of inl(x) => s(x) | inr(y) => t(y), True, <a, b>, P  Q, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), if b then t else f fi , {T}, s ~ t, SQType(T), A c B, x:A. B(x), (x  l), x. t(x), ff, b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], p  q, p  q, p q, tt, A List, x(s)

Lemmas

member-insert-by, l all cons, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, sorted-by-cons, l all wf, l member wf, guard wf, false wf, true wf, unit wf, subtype rel wf, length wf1, member wf, int seg wf, select wf, length wf2, bool wf, iff wf, linorder wf, insert-by wf, assert wf, sorted-by wf